l:(Top List), i:, x:Top. ||l[i:=x]|| ~ ||l|| 

latex

Definitions	Top, t  T, x:A. B(x), ||as||, l[i:=x], A  B, P & Q, i  j < k, P  Q, False, A, {i..j}, l[i], (i = j), f[x:=v], i  j , , , b, b, , P  Q, Unit, {T}, SQType(T)
Lemmas	eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bool wf, bnot wf, not wf, assert wf, mklist length, non neg length, update wf, eq int wf, select wf, int seg wf, le wf, length wf1, top wf